Technical Field
This disclosure generally relates to formal verification. More specifically, this disclosure relates to equivalence checking between two or more circuit designs that include division or square root circuits.
Related Art
The importance of circuit verification cannot be over-emphasized. Indeed, without circuit verification it would have been practically impossible to design complicated integrated circuits (ICs) which are commonly found in today's computing devices.
Circuits that perform division and that compute a square root are used extensively in ICs. For example, these circuits are commonly used in central processing units (CPUs), graphics processors, digital signal processors, etc. There have been many cases in which a bug in a circuit implementation of a mathematical operator had a significant impact on the company's finances. For example, in one well-publicized instance, a bug in a floating-point division circuit cost the company hundreds of millions of dollars. Therefore, it is very important to guarantee that certain circuits (e.g., division and square root circuits) in an IC will operate correctly.
An important problem in the area of formal verification involves equivalence checking between two or more circuit designs that are specified at the same or different abstraction levels. For example, equivalence checking can be performed between two register transfer level (RTL) designs or a design that is specified in a high-level programming language (e.g., C++) and an RTL design.
One approach for checking equivalence between two or more circuit designs is to exhaustively simulate the two or more circuit designs over all possible inputs to ensure that the two or more circuit designs produce the same output whenever their inputs are the same. However, this approach is clearly impractical because it is computationally infeasible (and often impossible) to exhaustively simulate non-trivial circuit designs such division circuit designs and square-root circuit designs.
Another approach is to use formal verification to prove equivalence between the two or more circuit designs. Unfortunately, naïve formal verification based approaches can have serious runtime and memory issues when they are used to prove equivalence between two or more circuit designs that include a division circuit and/or a square-root circuit. Hence, what is needed are techniques and systems to efficiently perform formal equivalence checking between two or more circuit designs that include a division circuit and/or a square-root circuit without the above-described problems.